\newcommand{\codeIsEqualTo}{\quad%
     \ensuremath{=}\quad\hspace{-0.6em}}

\newcommand{\codeIsEqualToInContext}[2]{\quad%
     \ensuremath{=_{#1,#2}}\quad\hspace{-0.6em}}

\newcommand{\codeIsEqualToInContextDois}{\quad\quad\quad%
     \ensuremath{=}\quad\quad\quad\hspace{-0.6em}}

\newcommand{\codeIsEqualToInText}[2]{\quad\hspace{-1em}%
     \ensuremath{=_{#1,#2}}\quad\hspace{-1em}}

\newcommand{\codeIsARefinamentOfInText}[2]{\quad\hspace{-1em}%
     \ensuremath{\sqsubseteq_{#1,#2}}\quad\hspace{-1em}}

\newcommand{\codeIsARefinamentOfInContext}[2]{\quad%
     \ensuremath{\sqsubseteq_{#1,#2}}\quad\hspace{-0.6em}}

\newcommand{\cmdIsEqualToInContext}{\quad%
     \ensuremath{=}\quad\hspace{2.0em}}

\newcommand{\cmdIsEqualToInContextDois}{\quad\quad\quad\quad\quad%
     \ensuremath{=}\quad\hspace{1.0em}}

\newcommand{\cmdSpaceToInContext}{\quad%
     \ensuremath{ }\quad\hspace{2.0em}}

\newcommand{\subclassOp}{\ensuremath{\leq} }
\newcommand{\notSubclassOp}{\ensuremath{\nleq} }
\newcommand{\implica}{\ensuremath{\Rightarrow} }

\newcommand{\pindent}{\hspace{1.5em}}

\newcommand{\cc}[1]{\ensuremath{#1}}
\newcommand{\keywordFont}[1]{\ensuremath{\mathbf{#1}}}

\newcommand{\isDefinedBy}{\hspace{0.15em}\ensuremath{\sdef}\hspace{0.15em}}

\newcommand{\specCases}{$@spec\_cases$}
\newcommand{\also}{\keywordFont{also}}
\newcommand{\invariant}{\keywordFont{invariant}}
\newcommand{\requires}{\keywordFont{requires}}
\newcommand{\assignable}{\keywordFont{assignable}}
\newcommand{\ensures}{\keywordFont{ensures}}
\newcommand{\btrue}{\keywordFont{true}}
\newcommand{\bfalse}{\keywordFont{false}}
\newcommand{\class}{\keywordFont{class}}
\newcommand{\Abstract}{\keywordFont{abstract}}
\newcommand{\extends}{\keywordFont{extends}}
\newcommand{\private}{\keywordFont{private}}
\newcommand{\public}{\keywordFont{public}}
\newcommand{\Protected}{\keywordFont{protected}}
\newcommand{\classEnd}{\keywordFont{\}}}
\newcommand{\guardStart}{\keywordFont{\{}}
\newcommand{\guardEnd}{\keywordFont{\}}}
\newcommand{\methodstart}{\keywordFont{m}}
\newcommand{\switch}{\keywordFont{switch}}
\newcommand{\Case}{\keywordFont{case}}
\newcommand{\default}{\keywordFont{default}}
\newcommand{\If}{\keywordFont{if}}
\newcommand{\Object}{\keywordFont{Object}}
\newcommand{\Assert}{\keywordFont{assert}}
\newcommand{\Null}{\keywordFont{null}}
\newcommand{\This}{\keywordFont{this}}
\newcommand{\Super}{\keywordFont{super}}
\newcommand{\instanceof}{\keywordFont{instanceof}}
\newcommand{\Return}{\keywordFont{return}}
\newcommand{\Else}{\keywordFont{else}}
\newcommand{\new}{\keywordFont{new}}
\newcommand{\barraOld}{$\backslash$\keywordFont{old}}
\newcommand{\notSpecified}{$\backslash$\keywordFont{not\_specified}}
\newcommand{\same}{$\backslash$\keywordFont{same}}
\newcommand{\nothing}{$\backslash$\keywordFont{nothing}}
\newcommand{\barraResult}{\backslash$result$}
\newcommand{\barraResultDois}{$\backslash result$ }

\newcommand{\providedJava}{\item[\textbf{\textit{Java:}}]}
\newcommand{\providedJml}{\item[\textbf{\textit{JML:}}]}

\newcommand{\specPublic}{\keywordFont{spec\_public}}
\newcommand{\specProtected}{\keywordFont{spec\_protected}}
\newcommand{\pure}{\keywordFont{pure}}
\newcommand{\specStart}{$/*@$}
\newcommand{\specLine}{$@$}
\newcommand{\specEnd}{$@*/$}

\newcommand{\singleSpec}{$//@$}

\newcommand{\subescrito}[2]{$#1_#2$}

\newcommand{\refJmlLaw}[1]{\textbf{Law #1}}

\newcommand{\refJavaLaw}[1]{\textbf{Law #1}}

\newcommand{\refJavaJmlLaw}[1]{\textbf{Law #1}}

\newcommand{\refJavaJml}[1]{\textbf{#1}}

\newcommand{\refFigura}[1]{\textbf{Figure \ref{#1}}}

\newcommand{\printLawTitle}[1]{\ensuremath{\textbf{Law} \langle}\textit{#1}%
                         \ensuremath{\rangle}}
\newcommand{\fleri}{(l/r) }
\newcommand{\frile}{(r/l) }

% -------------------------------------- %

\newlength{\codeLength}
\newsavebox{\fminibox}
\newlength{\fminilength}
\newenvironment{fminipage}[1][\linewidth]
   {\setlength{\fminilength}{#1-2\fboxsep-2\fboxrule}
    \begin{lrbox}{\fminibox}\begin{minipage}{\fminilength}}
   {\end{minipage}\end{lrbox}\noindent\fbox{\usebox{\fminibox}}}
\newenvironment{framedCode}
     {%
      %\settowidth{\codeLength}{#1}
      %
      \setlength{\codeLength}{0.41\linewidth}
      \begin{fminipage}[\codeLength]      
      \begin{alltt}}
     {\end{alltt}
      \end{fminipage}}

\newenvironment{unframedCode}
     {%
      %\settowidth{\codeLength}{#1}
      %
      \setlength{\codeLength}{0.35\linewidth}
      \begin{minipage}{\codeLength}   
      \begin{alltt}}
     {\end{alltt}
      \end{minipage}}

\newtheorem{law}{Law}

\newtheorem{jmllaw}{Law}

\newtheorem{javajmllaw}{Law}

\newcommand{\lawName}[1]{\hspace{-0.5em}\textbf{A}\ensuremath{\langle}\textit{#1}%
                         \ensuremath{\rangle}}
\newenvironment{Law}[1]
   {\begin{law} \normalfont \lawName{#1} \\ \noindent}
   {\hfill $\Box$\end{law}}

\newcommand{\lawJmlName}[1]{\hspace{-0.5em}\ensuremath{\langle}\textit{#1}%
                         \ensuremath{\rangle}}
\newenvironment{LawJml}[1]
   {\begin{jmllaw} \normalfont \lawJmlName{#1} \\ \noindent}
   {\hfill $\Box$\end{jmllaw}}

\newcommand{\lawJavaJmlName}[1]{\hspace{-0.5em}\ensuremath{\langle}\textit{#1}%
                         \ensuremath{\rangle}}
\newenvironment{LawJavaJml}[1]
   {\begin{javajmllaw} \normalfont \lawJavaJmlName{#1} \\ \noindent}
   {\hfill $\Box$\end{javajmllaw}}
